Code and Notes (Week 8 Tuesday)

-- Week 8A: Parametric Polymorphism in Haskell
module Main where
import Data.Typeable

-- a polymorphic datatype and function
data MyList a = MyNil | MyCons a (MyList a)
  deriving Show -- this allows printing the datatype

toMyList :: a -> MyList a
toMyList x = MyCons x MyNil

-- a monomorphic swap function
swapInts :: (Int,Int) -> (Int,Int)
swapInts p = (snd p, fst p)

-- a polymorphic swap function
swap :: (a,b) -> (b,a)
swap p = (snd p, fst p)

-- Polymorphic recursion example
data Dims a = Step a (Dims [a]) | Epsilon
  deriving Show

-- Example Dims value, from the slide
-- NB: Can use :t in ghci to display type of a term
mydims :: Dims Int
mydims = Step 1 (Step [1, 2] (Step [[1, 2], [3, 4]] Epsilon))

-- A summing function on Dims, from the slide
sumDims :: (a -> Int) -> Dims a -> Int
sumDims f Epsilon = 0
sumDims f (Step x t) = (f x) + sumDims (sum . map f) t

-- Parametricity and constraints on implementations
-- How many implementations?
foo :: Int -> Int
-- foo x = undefined -- define me!
-- We thought of a few! With basically infinite variations:
-- foo x = x + 1 -- you could have as many variations on this
--                  as you have constant Int values
foo x = x * x -- you could take x^n for any n
-- etc...
-- How about this one?
goo :: a -> a
-- goo x = undefined -- define me!
-- We only found one:
goo x = x

-- Today's class also made another interesting suggestion
-- for `goo :: a -> a` - Why not case split on whether
-- the input is a particular value of a given type?
--   But we found we were forced to specify further that `a`
-- belongs to various typeclasses like Num and Eq, for goo2
-- to be able to refer to specific values of it like 4, 5
-- and to be able to check equality for pattern matching.
--   So, in line with the parametricity principle, we still
-- can't refer to values without some loss of generality.
goo2 :: Num a => Eq a => a -> a
goo2 x = case x of
  4 -> 5
  _ -> x

-- Other questions raised by students in class today:

-- Q1: The "HM Types" slide made the point that a function's
-- polymorphism is "not Hindley-Milner" if forall-quantifiers
-- occur in the not-outermost part of a type declaration.
--
-- Q1a: What's an example of this?
--    Here's the one we found, thanks to Q3b below:
--      test1 :: (forall a. [a] -> Int) -> Int
--
-- Q1b: Is this example implementable in Haskell?
--    Yes - see more on test1 below.
--
-- Another student suggestion for Q1a and Q1b was
--   something :: forall a. a -> (forall b. b -> b)
-- implemented roughly as follows
--   if we get an int, return id function for bools
--   if we get a bool, return id function for ints
-- with the suggestion we could perhaps implement this
-- using Data.Typeable and typeOf. But it turns out,
-- even if Typeable typeclass shenanigans allow us
-- to case split on the input a's type, `something`'s
-- only suitable return value to satisfy polymorphic
--   (forall b. b -> b)
-- is still the polymorphic `id` function.
something :: Typeable a => a -> (forall b. b -> b)
something x = case show (typeOf(x)) of
  "Integer" -> id -- try in ghci: show (typeOf 42)
  "Bool" -> id -- try in ghci: show (typeOf False)
  _ -> id
-- And it looks having `forall b` on the right is
-- isomorphic to having it in outer position anyway
-- (see Q3a's proof1, proof2 for another example).
something1 :: (forall a. a -> (forall b. b -> b)) -> 
  (forall a b. a -> b -> b)
something1 f = \x -> id
something2 :: (forall a b. a -> b -> b) ->
  (forall a. a -> (forall b. b -> b))
something2 f = \x -> id
-- Remember, backslash used like this (\_ -> blah) is 
-- Haskell for lambda expression (λ_. blah).

-- Q2: Would mutual recursion between two types catch instances
-- of the second type invoking the first with different type
-- parameters as the first time?
--
-- Well, it looks like Haskell is perfectly happy to accept
-- a mutually recursive definition that results in differing
-- instantiations for `a` every time we recurse into Even :)
data Even a = EvenNil | EvenSucc a (Odd a)
  deriving Show
data Odd a = OddSucc a (Even [a])
  deriving Show
myeven :: Even Int
myeven = EvenSucc 1 (OddSucc 2 (EvenSucc [3] (OddSucc [4] EvenNil)))
-- But note, Haskell doesn't apply the HM restrictions anyway.
--
-- I suppose the real question was whether this violates HM
-- because technically this doesn't violate the wording of
-- the "HM Types" slide's 2nd restriction. Here, Even isn't
-- "calling itself with a different type parameter", but it
-- sort of will cause that to happen via Odd.
--
-- My tentative answer is that Even/Odd here isn't HM
-- polymorphic for type variable `a` (even rules-lawyering
-- the restriction on the slide) because, just like Dims,
-- `a` isn't statically instantiable because its number of
-- instantiations depends on runtime depths of Even/Odd.

-- Q3: According to this source on impredicative types,
--   https://wiki.haskell.org/Impredicative_types
-- Q3a: These two types:
--   Int -> forall a. a -> [a]
-- and
--   forall a. Int -> a -> [a]
-- are "actually the same". Why?

-- Student suggestion: A function `example n x` that returns a
-- list with n copies of x should satisfy both type signatures.
-- Apparently, Haskell's Data.List replicate does this.
example1 :: Int -> forall a. a -> [a]
example1 n x = replicate n x -- list with n copies of x
example2 :: forall a. Int -> a -> [a]
example2 n x = replicate n x -- list with n copies of x
-- So, it looks like it does satisfy both signatures.
-- Also, in ghci `:t replicate` shows that
--   replicate :: Int -> a -> [a]

-- If they are isomorphic, in principle we should be able to
-- implement both of these conversion functions between them.
-- If both functions are terminating, this constitutes a
-- proof that the two types/propositions are equivalent.
proof1 :: (Int -> forall a. a -> [a]) ->
  (forall a. Int -> a -> [a])
proof1 f = \i g -> f i g
-- `:t (proof1 example1)` in ghci gives us:
--   (proof1 example1) :: Int -> a -> [a]
-- So far so good.
proof2 :: (forall a. Int -> a -> [a]) ->
  (Int -> forall a. a -> [a]) 
proof2 f = \i g -> f i g
-- and, `:t (proof2 example2)` in ghci gives us:
--   (proof2 example2) :: Int -> forall a. a -> [a]
-- So we're done.

-- Q3b. The same source above says that the types
--   (forall a. [a] -> Int) -> Int
-- and
--   forall a. ([a] -> Int) -> Int
-- "really are" different. Why?

-- Both take a function of form `[a] -> Int`
-- and return an integer. But the class worked out
-- the difference is the first has to receive a
-- function f that is polymorphic for all `a`.
test1 :: (forall a. [a] -> Int) -> Int
test1 f = f [] -- this implementation is valid for both types
-- The below implementation also works because we already
-- know from the type signature that f works for all a,
-- so we know that it will work for a list of Ints.
--test1 f = f [1,2] -- valid impl. for this type
--
-- But the second can take a function that doesn't
-- itself have to be polymorphic for all `a`.
test2 :: forall a. ([a] -> Int) -> Int
test2 f = f [] -- this implementation is valid for both types
-- The below implementation gets a compile error because
-- test2 cannot assume anything about `a` that f supports.
-- For example:
--   f :: [Int] -> Int
--   f :: [Bool] -> Int
-- might both be valid types for the f that's given to test2.
-- So we don't know that f will accept [1,2] below:
--test2 f = f [1,2] -- compile error!

-- Another way to distinguish between the types
-- for test1 and test2: in ghci,
--   test1 lengthOfIntList  -- fails with type error
--   test2 lengthOfIntList  -- succeeds
-- because test1 demands that f be polymorphic,
-- and lengthOfIntList isn't.
lengthOfIntList :: [Int] -> Int
lengthOfIntList xs = length xs
-- Note also `test1 length` succeeds, because Haskell's
-- built-in `length` function is polymorphic enough.

-- Q4: If we could pattern match on types then could we
-- conceivably have type-specific behaviour?
--
-- goo3 :: a -> a -- compile error with this type signature!
goo3 x = case show (typeOf(x)) of
  "Integer" -> 4
  _ -> x
-- Yes, Haskell allows it. But if you `:t goo3` in ghci
-- you can see that it places further restrictions
-- on the type of `a`, so we have a resulting loss of
-- generality as described earlier.
--   goo3 :: (Typeable a, Num a) => a -> a

-- Q5: Could we use type classes somehow to address above?
--
-- Yes, as seen above we can constrain the polymorphism of
-- type variables by specifying they're typeclass Num etc.
-- to gain the ability to refer to values - but of course,
-- in exchange we lose the generality of the polymorphism.

-- For completeness, so the module can be compiled
main :: IO ()
main = putStrLn $ "Hello Week 8!"